FDL - Nuprl Lemma : increasing_split

Nuprl Lemma : increasing_split

m:

, P:(

m

Prop).
(

i:

m. Dec(P(i)))

(

n, k:

, f:(

n

m), g:(

k

m).

(increasing(f;n)

(& increasing(g;k)

(& (

i:

n. P(f(i)))

(& (

j:

k.

P(g(j)))

(& (

i:

m. (

j:

n. i = f(j)

)

(

j:

k. i = g(j)

)))

Definitions P Q, AB, A, False, P & Q, x:A. B(x), increasing(f;k), Dec(P), Prop, {i..j}, ij, P Q, x:A. B(x), t T, , S T, S T, i j < k, f[n:=x], True, if b t else f fi, Unit, P Q, i=j, T, , b, b, {T}

Lemmas decidable int equal, assert wf, bnot wf, true wf, squash wf, eq int wf, bool wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, fappend wf, le wf, id increasing, not wf, int seg wf, increasing wf, decidable wf, nat wf, nat properties, ge wf